﻿open System
open LambdaCalc

let mutable delayBodyReduction = false
let mutable cancellationToken : Threading.CancellationToken option = None

let dictionaryEnv =
    let dict = new System.Collections.Generic.Dictionary<_,_>()
    { new Parser.IParserEnvironment with
        member i.LoadExpression id = dict.[id]
        member i.StoreExpression (id, expr) = dict.[id] <- expr
        member i.KnownIdentifiers = dict |> Seq.map (fun kvp -> kvp.Key)
        member i.CoreParameters = 
            { 
                DelayAbstractionBodyReduction = delayBodyReduction
                CancelProcessingToken = cancellationToken
            }
    }


let tryLoadFile (fileName : string) : (string seq) option =
    let name =
        if System.IO.Path.GetExtension(fileName) <> ".lcs" 
        then fileName + ".lcs"
        else fileName
    if System.IO.File.Exists name then
        try
            System.IO.File.ReadAllLines name |> Array.toSeq |> Some
        with
        | :? System.IO.IOException -> None
    else
        None

let readEval (environment : Parser.IParserEnvironment) =
    printf ">>> "
    let input = Console.ReadLine()
    let printKnownIdentifiers (ids : string list) =
        if ids.Length > 0 then
            printf "== ["
            Console.ForegroundColor <- ConsoleColor.DarkMagenta
            printf "%s" (System.String.Join(", ", ids |> List.toArray))
            Console.ResetColor()     
            printfn "]\n"
    let rec eval input =   
        match Parser.LambdaParser.interpret environment input with
        | Parser.InterpreterResult.Command cmd
            -> match cmd with
               | Parser.InterpreterCommands.Quit 
                    -> false
               | Parser.InterpreterCommands.Load file
                    -> match tryLoadFile file with
                       | Some inputs
                            -> inputs |> Seq.fold (fun ok input -> (eval input) && ok) true
                        | None
                            -> printfn "could not load file %s" file
                               true
               | Parser.EnableBodyReductionDelay
                -> let message =
                    "abstractionsbodys will not be reduced on occurence\n"
                        + "this enables definition of recursive functions\n"
                        + "but disables extended term equality detection"
                   Console.WriteLine message
                   delayBodyReduction <- true
                   true
        | Parser.InterpreterResult.Success (expression, knownIdentifier)
            -> printfn "%s" (expression.ToString())
               knownIdentifier |> printKnownIdentifiers
               true
        | Parser.InterpreterResult.Failure failure
            -> Console.ForegroundColor <- ConsoleColor.Red
               printfn "- FAILURE -"
               printfn "%s" (failure.Message)
               printfn "-----------"
               Console.ResetColor()
               true
        | Parser.InterpreterResult.Comparision (result, _)  
            -> printfn "%A" result
               true
    eval input
    
let rec readEvalLoop() =
    let c = readEval dictionaryEnv
    printfn ""
    if c then readEvalLoop()

[<EntryPoint>]
let main argv = 
    printfn "LAMBDA CALCULUS INTERPRETER"
    printfn "==========================="
    printfn ""; printfn ""

    readEvalLoop()   
    0 // return an integer exit code
